<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Sub: Subtyping</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: 编程语言基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Sub<span class="subtitle">Subtyping</span></h1>


<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Strings.String</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="keyword">Types</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/>
</div>

<div class="doc">
<a name="lab283"></a><h1 class="section">Concepts</h1>

<div class="paragraph"> </div>

 We now turn to the study of _subtyping_, a key feature
    needed to support the object-oriented programming style. 
</div>

<div class="doc">
<a name="lab284"></a><h2 class="section">A Motivating Example</h2>

<div class="paragraph"> </div>

 Suppose we are writing a program involving two record types
    defined as follows:
<pre>
      Person  = {name:String, age:Nat}
      Student = {name:String, age:Nat, gpa:Nat}
</pre>

<div class="paragraph"> </div>

 In the simply typed lamdba-calculus with records, the term
<pre>
      (\r:Person. (r.age)+1) {name="Pat",age=21,gpa=1}
</pre>
   is not typable, since it applies a function that wants a two-field
   record to an argument that actually provides three fields, while the
   <span class="inlinecode"><span class="id" type="var">T_App</span></span> rule demands that the domain type of the function being
   applied must match the type of the argument precisely.

<div class="paragraph"> </div>

   But this is silly: we're passing the function a _better_ argument
   than it needs!  The only thing the body of the function can
   possibly do with its record argument <span class="inlinecode"><span class="id" type="var">r</span></span> is project the field <span class="inlinecode"><span class="id" type="var">age</span></span>
   from it: nothing else is allowed by the type, and the presence or
   absence of an extra <span class="inlinecode"><span class="id" type="var">gpa</span></span> field makes no difference at all.  So,
   intuitively, it seems that this function should be applicable to
   any record value that has at least an <span class="inlinecode"><span class="id" type="var">age</span></span> field.

<div class="paragraph"> </div>

   More generally, a record with more fields is "at least as good in
   any context" as one with just a subset of these fields, in the
   sense that any value belonging to the longer record type can be
   used _safely_ in any context expecting the shorter record type.  If
   the context expects something with the shorter type but we actually
   give it something with the longer type, nothing bad will
   happen (formally, the program will not get stuck).

<div class="paragraph"> </div>

   The principle at work here is called _subtyping_.  We say that "<span class="inlinecode"><span class="id" type="var">S</span></span>
   is a subtype of <span class="inlinecode"><span class="id" type="var">T</span></span>", written <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>, if a value of type <span class="inlinecode"><span class="id" type="var">S</span></span> can
   safely be used in any context where a value of type <span class="inlinecode"><span class="id" type="var">T</span></span> is
   expected.  The idea of subtyping applies not only to records, but
   to all of the type constructors in the language &mdash; functions,
   pairs, etc. 
<div class="paragraph"> </div>

 Safe substitution principle:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">S</span></span> is a subtype of <span class="inlinecode"><span class="id" type="var">T</span></span>, written <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>, if a value of type
         <span class="inlinecode"><span class="id" type="var">S</span></span> can safely be used in any context where a value of type
         <span class="inlinecode"><span class="id" type="var">T</span></span> is expected.

</li>
</ul>

<div class="paragraph"> </div>

<a name="lab285"></a><h2 class="section">Subtyping and Object-Oriented Languages</h2>

<div class="paragraph"> </div>

 Subtyping plays a fundamental role in many programming
    languages &mdash; in particular, it is closely related to the notion of
    _subclassing_ in object-oriented languages.

<div class="paragraph"> </div>

    An _object_ in Java, C<span class="inlinecode">#</span>, etc. can be thought of as a record,
    some of whose fields are functions ("methods") and some of whose
    fields are data values ("fields" or "instance variables").
    Invoking a method <span class="inlinecode"><span class="id" type="var">m</span></span> of an object <span class="inlinecode"><span class="id" type="var">o</span></span> on some arguments <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>..<span class="id" type="var">an</span></span>
    roughly consists of projecting out the <span class="inlinecode"><span class="id" type="var">m</span></span> field of <span class="inlinecode"><span class="id" type="var">o</span></span> and
    applying it to <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>..<span class="id" type="var">an</span></span>.

<div class="paragraph"> </div>

    The type of an object is called a _class_ &mdash; or, in some
    languages, an _interface_.  It describes which methods and which
    data fields the object offers.  Classes and interfaces are related
    by the _subclass_ and _subinterface_ relations.  An object
    belonging to a subclass (or subinterface) is required to provide
    all the methods and fields of one belonging to a superclass (or
    superinterface), plus possibly some more.

<div class="paragraph"> </div>

    The fact that an object from a subclass can be used in place of
    one from a superclass provides a degree of flexibility that is
    extremely handy for organizing complex libraries.  For example, a
    GUI toolkit like Java's Swing framework might define an abstract
    interface <span class="inlinecode"><span class="id" type="var">Component</span></span> that collects together the common fields and
    methods of all objects having a graphical representation that can
    be displayed on the screen and interact with the user, such as the
    buttons, checkboxes, and scrollbars of a typical GUI.  A method
    that relies only on this common interface can now be applied to
    any of these objects.

<div class="paragraph"> </div>

    Of course, real object-oriented languages include many other
    features besides these.  For example, fields can be updated.
    Fields and methods can be declared <span class="inlinecode"><span class="id" type="var">private</span></span>.  Classes can give
    _initializers_ that are used when constructing objects.  Code in
    subclasses can cooperate with code in superclasses via
    _inheritance_.  Classes can have static methods and fields.  Etc.,
    etc.

<div class="paragraph"> </div>

    To keep things simple here, we won't deal with any of these
    issues &mdash; in fact, we won't even talk any more about objects or
    classes.  (There is a lot of discussion in <a href="Bib.html#Pierce 2002"><span class="inlineref">[Pierce 2002]</span></a>, if
    you are interested.)  Instead, we'll study the core concepts
    behind the subclass / subinterface relation in the simplified
    setting of the STLC. 
<div class="paragraph"> </div>

<a name="lab286"></a><h2 class="section">The Subsumption Rule</h2>

<div class="paragraph"> </div>

 Our goal for this chapter is to add subtyping to the simply typed
    lambda-calculus (with some of the basic extensions from <span class="inlinecode"><span class="id" type="var">MoreStlc</span></span>).
    This involves two steps:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Defining a binary _subtype relation_ between types.

<div class="paragraph"> </div>


</li>
<li> Enriching the typing relation to take subtyping into account.

</li>
</ul>

<div class="paragraph"> </div>

    The second step is actually very simple.  We add just a single rule
    to the typing relation: the so-called _rule of subsumption_:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;S&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;S&nbsp;<:&nbsp;T</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Sub) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;T</td>
  <td></td>
</td>
</table></center>    This rule says, intuitively, that it is OK to "forget" some of
    what we know about a term. 
<div class="paragraph"> </div>

 For example, we may know that <span class="inlinecode"><span class="id" type="var">t</span></span> is a record with two
    fields (e.g., <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">x</span>:<span class="id" type="var">A</span>→<span class="id" type="var">A</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">B</span>→<span class="id" type="var">B</span>}</span>), but choose to forget about
    one of the fields (<span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">y</span>:<span class="id" type="var">B</span>→<span class="id" type="var">B</span>}</span>) so that we can pass <span class="inlinecode"><span class="id" type="var">t</span></span> to a
    function that requires just a single-field record. 
<div class="paragraph"> </div>

<a name="lab287"></a><h2 class="section">The Subtype Relation</h2>

<div class="paragraph"> </div>

 The first step &mdash; the definition of the relation <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> &mdash; is
    where all the action is.  Let's look at each of the clauses of its
    definition.  
<div class="paragraph"> </div>

<a name="lab288"></a><h3 class="section">Structural Rules</h3>

<div class="paragraph"> </div>

 To start off, we impose two "structural rules" that are
    independent of any particular type constructor: a rule of
    _transitivity_, which says intuitively that, if <span class="inlinecode"><span class="id" type="var">S</span></span> is
    better (richer, safer) than <span class="inlinecode"><span class="id" type="var">U</span></span> and <span class="inlinecode"><span class="id" type="var">U</span></span> is better than <span class="inlinecode"><span class="id" type="var">T</span></span>,
    then <span class="inlinecode"><span class="id" type="var">S</span></span> is better than <span class="inlinecode"><span class="id" type="var">T</span></span>...
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;U&nbsp;&nbsp;&nbsp;&nbsp;U&nbsp;<:&nbsp;T</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Trans) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;T</td>
  <td></td>
</td>
</table></center>    ... and a rule of _reflexivity_, since certainly any type <span class="inlinecode"><span class="id" type="var">T</span></span> is
    as good as itself:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Refl) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">T&nbsp;<:&nbsp;T</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

<a name="lab289"></a><h3 class="section">Products</h3>

<div class="paragraph"> </div>

 Now we consider the individual type constructors, one by one,
    beginning with product types.  We consider one pair to be a subtype
    of another if each of its components is.
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Prod) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;*&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;*&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

<a name="lab290"></a><h3 class="section">Arrows</h3>

<div class="paragraph"> </div>

 The subtyping rule for arrows is a little less intuitive.
    Suppose we have functions <span class="inlinecode"><span class="id" type="var">f</span></span> and <span class="inlinecode"><span class="id" type="var">g</span></span> with these types:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span>&nbsp;:&nbsp;<span class="id" type="var">C</span>&nbsp;→&nbsp;<span class="id" type="var">Student</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span>&nbsp;:&nbsp;(<span class="id" type="var">C</span>→<span class="id" type="var">Person</span>)&nbsp;→&nbsp;<span class="id" type="var">D</span>
<div class="paragraph"> </div>

</div>
    That is, <span class="inlinecode"><span class="id" type="var">f</span></span> is a function that yields a record of type <span class="inlinecode"><span class="id" type="var">Student</span></span>,
    and <span class="inlinecode"><span class="id" type="var">g</span></span> is a (higher-order) function that expects its argument to be
    a function yielding a record of type <span class="inlinecode"><span class="id" type="var">Person</span></span>.  Also suppose that
    <span class="inlinecode"><span class="id" type="var">Student</span></span> is a subtype of <span class="inlinecode"><span class="id" type="var">Person</span></span>.  Then the application <span class="inlinecode"><span class="id" type="var">g</span></span> <span class="inlinecode"><span class="id" type="var">f</span></span> is
    safe even though their types do not match up precisely, because
    the only thing <span class="inlinecode"><span class="id" type="var">g</span></span> can do with <span class="inlinecode"><span class="id" type="var">f</span></span> is to apply it to some
    argument (of type <span class="inlinecode"><span class="id" type="var">C</span></span>); the result will actually be a <span class="inlinecode"><span class="id" type="var">Student</span></span>,
    while <span class="inlinecode"><span class="id" type="var">g</span></span> will be expecting a <span class="inlinecode"><span class="id" type="var">Person</span></span>, but this is safe because
    the only thing <span class="inlinecode"><span class="id" type="var">g</span></span> can then do is to project out the two fields
    that it knows about (<span class="inlinecode"><span class="id" type="var">name</span></span> and <span class="inlinecode"><span class="id" type="var">age</span></span>), and these will certainly
    be among the fields that are present.

<div class="paragraph"> </div>

    This example suggests that the subtyping rule for arrow types
    should say that two arrow types are in the subtype relation if
    their results are:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Arrow_Co) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;→&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;S<sub>1</sub>&nbsp;→&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

    We can generalize this to allow the arguments of the two arrow
    types to be in the subtype relation as well:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">T<sub>1</sub>&nbsp;<:&nbsp;S<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Arrow) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;→&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;→&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center>    But notice that the argument types are subtypes "the other way round":
    in order to conclude that <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span>→<span class="id" type="var">S<sub>2</sub></span></span> to be a subtype of <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span>→<span class="id" type="var">T<sub>2</sub></span></span>, it
    must be the case that <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> is a subtype of <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>.  The arrow
    constructor is said to be _contravariant_ in its first argument
    and _covariant_ in its second.

<div class="paragraph"> </div>

    Here is an example that illustrates this:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span>&nbsp;:&nbsp;<span class="id" type="var">Person</span>&nbsp;→&nbsp;<span class="id" type="var">C</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span>&nbsp;:&nbsp;(<span class="id" type="var">Student</span>&nbsp;→&nbsp;<span class="id" type="var">C</span>)&nbsp;→&nbsp;<span class="id" type="var">D</span>
<div class="paragraph"> </div>

</div>
    The application <span class="inlinecode"><span class="id" type="var">g</span></span> <span class="inlinecode"><span class="id" type="var">f</span></span> is safe, because the only thing the body of
    <span class="inlinecode"><span class="id" type="var">g</span></span> can do with <span class="inlinecode"><span class="id" type="var">f</span></span> is to apply it to some argument of type
    <span class="inlinecode"><span class="id" type="var">Student</span></span>.  Since <span class="inlinecode"><span class="id" type="var">f</span></span> requires records having (at least) the
    fields of a <span class="inlinecode"><span class="id" type="var">Person</span></span>, this will always work. So <span class="inlinecode"><span class="id" type="var">Person</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span> is a
    subtype of <span class="inlinecode"><span class="id" type="var">Student</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span> since <span class="inlinecode"><span class="id" type="var">Student</span></span> is a subtype of
    <span class="inlinecode"><span class="id" type="var">Person</span></span>.

<div class="paragraph"> </div>

    The intuition is that, if we have a function <span class="inlinecode"><span class="id" type="var">f</span></span> of type <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span>→<span class="id" type="var">S<sub>2</sub></span></span>,
    then we know that <span class="inlinecode"><span class="id" type="var">f</span></span> accepts elements of type <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>; clearly, <span class="inlinecode"><span class="id" type="var">f</span></span>
    will also accept elements of any subtype <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> of <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>. The type of
    <span class="inlinecode"><span class="id" type="var">f</span></span> also tells us that it returns elements of type <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span>; we can
    also view these results belonging to any supertype <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> of
    <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span>. That is, any function <span class="inlinecode"><span class="id" type="var">f</span></span> of type <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span>→<span class="id" type="var">S<sub>2</sub></span></span> can also be
    viewed as having type <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span>→<span class="id" type="var">T<sub>2</sub></span></span>. 
<div class="paragraph"> </div>

<a name="lab291"></a><h3 class="section">Records</h3>

<div class="paragraph"> </div>

 What about subtyping for record types? 
<div class="paragraph"> </div>

 The basic intuition is that it is always safe to use a "bigger"
    record in place of a "smaller" one.  That is, given a record type,
    adding extra fields will always result in a subtype.  If some code
    is expecting a record with fields <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span>, it is perfectly safe
    for it to receive a record with fields <span class="inlinecode"><span class="id" type="var">x</span></span>, <span class="inlinecode"><span class="id" type="var">y</span></span>, and <span class="inlinecode"><span class="id" type="var">z</span></span>; the <span class="inlinecode"><span class="id" type="var">z</span></span>
    field will simply be ignored.  For example,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>,&nbsp;<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>,&nbsp;<span class="id" type="var">gpa</span>:<span class="id" type="var">Nat</span>}&nbsp;&lt;:&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>,&nbsp;<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>,&nbsp;<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>}&nbsp;&lt;:&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>}&nbsp;&lt;:&nbsp;{}
<div class="paragraph"> </div>

</div>
    This is known as "width subtyping" for records. 
<div class="paragraph"> </div>

 We can also create a subtype of a record type by replacing the type
    of one of its fields with a subtype.  If some code is expecting a
    record with a field <span class="inlinecode"><span class="id" type="var">x</span></span> of type <span class="inlinecode"><span class="id" type="var">T</span></span>, it will be happy with a record
    having a field <span class="inlinecode"><span class="id" type="var">x</span></span> of type <span class="inlinecode"><span class="id" type="var">S</span></span> as long as <span class="inlinecode"><span class="id" type="var">S</span></span> is a subtype of
    <span class="inlinecode"><span class="id" type="var">T</span></span>. For example,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id" type="var">x</span>:<span class="id" type="var">Student</span>}&nbsp;&lt;:&nbsp;{<span class="id" type="var">x</span>:<span class="id" type="var">Person</span>}
<div class="paragraph"> </div>

</div>
    This is known as "depth subtyping". 
<div class="paragraph"> </div>

 Finally, although the fields of a record type are written in a
    particular order, the order does not really matter. For example,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>,<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>}&nbsp;&lt;:&nbsp;{<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>,<span class="id" type="var">name</span>:<span class="id" type="var">String</span>}
<div class="paragraph"> </div>

</div>
    This is known as "permutation subtyping". 
<div class="paragraph"> </div>

 We _could_ formalize these requirements in a single subtyping rule
    for records as follows:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule"><span style='font-size:120%;'>&forall;</span>jk&nbsp;in&nbsp;j<sub>1</sub>..jn,</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule"><span style='font-size:120%;'>&exist;</span>ip&nbsp;in&nbsp;i<sub>1</sub>..im,&nbsp;such&nbsp;that</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">jk=ip&nbsp;and&nbsp;Sp&nbsp;<:&nbsp;Tk</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Rcd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...im:Sm}&nbsp;<:&nbsp;{j<sub>1</sub>:T<sub>1</sub>...jn:Tn}</td>
  <td></td>
</td>
</table></center>    That is, the record on the left should have all the field labels of
    the one on the right (and possibly more), while the types of the
    common fields should be in the subtype relation.

<div class="paragraph"> </div>

    However, this rule is rather heavy and hard to read, so it is often
    decomposed into three simpler rules, which can be combined using
    <span class="inlinecode"><span class="id" type="var">S_Trans</span></span> to achieve all the same effects. 
<div class="paragraph"> </div>

 First, adding fields to the end of a record type gives a subtype:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">n&nbsp;>&nbsp;m</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdWidth) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:T<sub>1</sub>...in:Tn}&nbsp;<:&nbsp;{i<sub>1</sub>:T<sub>1</sub>...im:Tm}</td>
  <td></td>
</td>
</table></center>    We can use <span class="inlinecode"><span class="id" type="var">S_RcdWidth</span></span> to drop later fields of a multi-field
    record while keeping earlier fields, showing for example that
    <span class="inlinecode">{<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>,<span class="id" type="var">name</span>:<span class="id" type="var">String</span>}</span> <span class="inlinecode">&lt;:</span> <span class="inlinecode">{<span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>}</span>. 
<div class="paragraph"> </div>

 Second, subtyping can be applied inside the components of a compound
    record type:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;...&nbsp;&nbsp;Sn&nbsp;<:&nbsp;Tn</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdDepth) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;<:&nbsp;{i<sub>1</sub>:T<sub>1</sub>...in:Tn}</td>
  <td></td>
</td>
</table></center>    For example, we can use <span class="inlinecode"><span class="id" type="var">S_RcdDepth</span></span> and <span class="inlinecode"><span class="id" type="var">S_RcdWidth</span></span> together to
    show that <span class="inlinecode">{<span class="id" type="var">y</span>:<span class="id" type="var">Student</span>,</span> <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">Nat</span>}</span> <span class="inlinecode">&lt;:</span> <span class="inlinecode">{<span class="id" type="var">y</span>:<span class="id" type="var">Person</span>}</span>. 
<div class="paragraph"> </div>

 Third, subtyping can reorder fields.  For example, we
    want <span class="inlinecode">{<span class="id" type="var">name</span>:<span class="id" type="var">String</span>,</span> <span class="inlinecode"><span class="id" type="var">gpa</span>:<span class="id" type="var">Nat</span>,</span> <span class="inlinecode"><span class="id" type="var">age</span>:<span class="id" type="var">Nat</span>}</span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">Person</span></span>.  (We
    haven't quite achieved this yet: using just <span class="inlinecode"><span class="id" type="var">S_RcdDepth</span></span> and
    <span class="inlinecode"><span class="id" type="var">S_RcdWidth</span></span> we can only drop fields from the _end_ of a record
    type.)  So we add:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;is&nbsp;a&nbsp;permutation&nbsp;of&nbsp;{j<sub>1</sub>:T<sub>1</sub>...jn:Tn}</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdPerm) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;<:&nbsp;{j<sub>1</sub>:T<sub>1</sub>...jn:Tn}</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 It is worth noting that full-blown language designs may choose not
    to adopt all of these subtyping rules. For example, in Java:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Each class member (field or method) can be assigned a single
      index, adding new indices "on the right" as more members are
      added in subclasses (i.e., no permutation for classes).

<div class="paragraph"> </div>


</li>
<li> A class may implement multiple interfaces &mdash; so-called "multiple
      inheritance" of interfaces (i.e., permutation is allowed for
      interfaces).

<div class="paragraph"> </div>


</li>
<li> In early versions of Java, a subclass could not change the
      argument or result types of a method of its superclass (i.e., no
      depth subtyping or no arrow subtyping, depending how you look at
      it). 
</li>
</ul>

<div class="paragraph"> </div>

<a name="lab292"></a><h4 class="section">练习：2 星, standard, recommended (arrow_sub_wrong)</h4>
 Suppose we had incorrectly defined subtyping as covariant on both
    the right and the left of arrow types:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Arrow_wrong) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;→&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;→&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center>    Give a concrete example of functions <span class="inlinecode"><span class="id" type="var">f</span></span> and <span class="inlinecode"><span class="id" type="var">g</span></span> with the following
    types...

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span>&nbsp;:&nbsp;<span class="id" type="var">Student</span>&nbsp;→&nbsp;<span class="id" type="var">Nat</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span>&nbsp;:&nbsp;(<span class="id" type="var">Person</span>&nbsp;→&nbsp;<span class="id" type="var">Nat</span>)&nbsp;→&nbsp;<span class="id" type="var">Nat</span>
<div class="paragraph"> </div>

</div>
    ... such that the application <span class="inlinecode"><span class="id" type="var">g</span></span> <span class="inlinecode"><span class="id" type="var">f</span></span> will get stuck during
    execution.  (Use informal syntax.  No need to prove formally that
    the application gets stuck.)

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_arrow_sub_wrong</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab293"></a><h3 class="section">Top</h3>

<div class="paragraph"> </div>

 Finally, it is convenient to give the subtype relation a maximum
    element &mdash; a type that lies above every other type and is
    inhabited by all (well-typed) values.  We do this by adding to the
    language one new type constant, called <span class="inlinecode"><span class="id" type="var">Top</span></span>, together with a
    subtyping rule that places it above every other type in the
    subtype relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Top) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;Top</td>
  <td></td>
</td>
</table></center>    The <span class="inlinecode"><span class="id" type="var">Top</span></span> type is an analog of the <span class="inlinecode"><span class="id" type="var">Object</span></span> type in Java and C#. 
</div>

<div class="doc">
<a name="lab294"></a><h3 class="section">Summary</h3>

<div class="paragraph"> </div>

 In summary, we form the STLC with subtyping by starting with the
    pure STLC (over some set of base types) and then...

<div class="paragraph"> </div>

<ul class="doclist">
<li> adding a base type <span class="inlinecode"><span class="id" type="var">Top</span></span>,

<div class="paragraph"> </div>


</li>
<li> adding the rule of subsumption
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;S&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;S&nbsp;<:&nbsp;T</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Sub) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;T</td>
  <td></td>
</td>
</table></center>      to the typing relation, and

<div class="paragraph"> </div>


</li>
<li> defining a subtype relation as follows:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;U&nbsp;&nbsp;&nbsp;&nbsp;U&nbsp;<:&nbsp;T</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Trans) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;T</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Refl) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">T&nbsp;<:&nbsp;T</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Top) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S&nbsp;<:&nbsp;Top</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Prod) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;*&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;*&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">T<sub>1</sub>&nbsp;<:&nbsp;S<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Arrow) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;→&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;→&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">n&nbsp;>&nbsp;m</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdWidth) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:T<sub>1</sub>...in:Tn}&nbsp;<:&nbsp;{i<sub>1</sub>:T<sub>1</sub>...im:Tm}</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;...&nbsp;&nbsp;Sn&nbsp;<:&nbsp;Tn</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdDepth) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;<:&nbsp;{i<sub>1</sub>:T<sub>1</sub>...in:Tn}</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;is&nbsp;a&nbsp;permutation&nbsp;of&nbsp;{j<sub>1</sub>:T<sub>1</sub>...jn:Tn}</td>
  <td class="infrulenamecol" rowspan="3">
    (S_RcdPerm) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>:S<sub>1</sub>...in:Sn}&nbsp;<:&nbsp;{j<sub>1</sub>:T<sub>1</sub>...jn:Tn}</td>
  <td></td>
</td>
</table></center>
</li>
</ul>

</div>

<div class="doc">
<a name="lab295"></a><h2 class="section">Exercises</h2>

<div class="paragraph"> </div>

<a name="lab296"></a><h4 class="section">练习：1 星, standard, optional (subtype_instances_tf_1)</h4>
 Suppose we have types <span class="inlinecode"><span class="id" type="var">S</span></span>, <span class="inlinecode"><span class="id" type="var">T</span></span>, <span class="inlinecode"><span class="id" type="var">U</span></span>, and <span class="inlinecode"><span class="id" type="var">V</span></span> with <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>
    and <span class="inlinecode"><span class="id" type="var">U</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">V</span></span>.  Which of the following subtyping assertions
    are then true?  Write _true_ or _false_ after each one.
    (<span class="inlinecode"><span class="id" type="var">A</span></span>, <span class="inlinecode"><span class="id" type="var">B</span></span>, and <span class="inlinecode"><span class="id" type="var">C</span></span> here are base types like <span class="inlinecode"><span class="id" type="var">Bool</span></span>, <span class="inlinecode"><span class="id" type="var">Nat</span></span>, etc.)

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">T</span>→<span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span>→<span class="id" type="var">S</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">Top</span>→<span class="id" type="var">U</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S</span>→<span class="id" type="var">Top</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(<span class="id" type="var">C</span>→<span class="id" type="var">C</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" type="var">A</span>*<span class="id" type="var">B</span>)</span>  <span class="inlinecode">&lt;:</span>  <span class="inlinecode">(<span class="id" type="var">C</span>→<span class="id" type="var">C</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" type="var">Top</span>*<span class="id" type="var">B</span>)</span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">T</span>→<span class="id" type="var">T</span>→<span class="id" type="var">U</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S</span>→<span class="id" type="var">S</span>→<span class="id" type="var">V</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(<span class="id" type="var">T</span>→<span class="id" type="var">T</span>)→<span class="id" type="var">U</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode">(<span class="id" type="var">S</span>→<span class="id" type="var">S</span>)→<span class="id" type="var">V</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">((<span class="id" type="var">T</span>→<span class="id" type="var">S</span>)→<span class="id" type="var">T</span>)→<span class="id" type="var">U</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode">((<span class="id" type="var">S</span>→<span class="id" type="var">T</span>)→<span class="id" type="var">S</span>)→<span class="id" type="var">V</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">S</span>*<span class="id" type="var">V</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span>*<span class="id" type="var">U</span></span>

</li>
</ul>

<div class="paragraph"> </div>

 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab297"></a><h4 class="section">练习：2 星, standard (subtype_order)</h4>
 The following types happen to form a linear order with respect to subtyping:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">Top</span></span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">Top</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Student</span></span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">Student</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Person</span></span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">Student</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Top</span></span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">Person</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Student</span></span>

</li>
</ul>

<div class="paragraph"> </div>

Write these types in order from the most specific to the most general.

<div class="paragraph"> </div>

Where does the type <span class="inlinecode"><span class="id" type="var">Top</span>→<span class="id" type="var">Top</span>→<span class="id" type="var">Student</span></span> fit into this order?
That is, state how <span class="inlinecode"><span class="id" type="var">Top</span></span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" type="var">Top</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Student</span>)</span> compares with each
of the five types above. It may be unrelated to some of them.  

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_subtype_order</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab298"></a><h4 class="section">练习：1 星, standard (subtype_instances_tf_2)</h4>
 Which of the following statements are true?  Write _true_ or
    _false_ after each one.

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>&nbsp;<span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T</span>&nbsp;&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>→<span class="id" type="var">S</span>&nbsp;&nbsp;&nbsp;&lt;:&nbsp;&nbsp;<span class="id" type="var">T</span>→<span class="id" type="var">T</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">A</span>→<span class="id" type="var">A</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;=&nbsp;<span class="id" type="var">T</span>→<span class="id" type="var">T</span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">T</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">A</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>&nbsp;<span class="id" type="var">T<sub>1</sub></span>&nbsp;<span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T<sub>1</sub></span>&nbsp;→&nbsp;<span class="id" type="var">T<sub>2</sub></span>)&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S<sub>1</sub></span>&nbsp;<span class="id" type="var">S<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;=&nbsp;<span class="id" type="var">S<sub>1</sub></span>&nbsp;→&nbsp;<span class="id" type="var">S<sub>2</sub></span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">T<sub>1</sub></span>&nbsp;&lt;:&nbsp;<span class="id" type="var">S<sub>1</sub></span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">S<sub>2</sub></span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T<sub>2</sub></span>&nbsp;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">S</span>→<span class="id" type="var">S</span>&nbsp;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>→<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">S</span>&nbsp;&nbsp;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>&nbsp;<span class="id" type="var">T<sub>1</sub></span>&nbsp;<span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T<sub>1</sub></span>*<span class="id" type="var">T<sub>2</sub></span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S<sub>1</sub></span>&nbsp;<span class="id" type="var">S<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;=&nbsp;<span class="id" type="var">S<sub>1</sub></span>*<span class="id" type="var">S<sub>2</sub></span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">S<sub>1</sub></span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T<sub>1</sub></span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">S<sub>2</sub></span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T<sub>2</sub></span>&nbsp;&nbsp;
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_subtype_instances_tf_2</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab299"></a><h4 class="section">练习：1 星, standard (subtype_concepts_tf)</h4>
 Which of the following statements are true, and which are false?

<div class="paragraph"> </div>

<ul class="doclist">
<li> There exists a type that is a supertype of every other type.

<div class="paragraph"> </div>


</li>
<li> There exists a type that is a subtype of every other type.

<div class="paragraph"> </div>


</li>
<li> There exists a pair type that is a supertype of every other
      pair type.

<div class="paragraph"> </div>


</li>
<li> There exists a pair type that is a subtype of every other
      pair type.

<div class="paragraph"> </div>


</li>
<li> There exists an arrow type that is a supertype of every other
      arrow type.

<div class="paragraph"> </div>


</li>
<li> There exists an arrow type that is a subtype of every other
      arrow type.

<div class="paragraph"> </div>


</li>
<li> There is an infinite descending chain of distinct types in the
      subtype relation&mdash;-that is, an infinite sequence of types
      <span class="inlinecode"><span class="id" type="var">S<sub>0</sub></span></span>, <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>, etc., such that all the <span class="inlinecode"><span class="id" type="var">Si</span></span>'s are different and
      each <span class="inlinecode"><span class="id" type="var">S</span>(<span class="id" type="var">i</span>+1)</span> is a subtype of <span class="inlinecode"><span class="id" type="var">Si</span></span>.

<div class="paragraph"> </div>


</li>
<li> There is an infinite _ascending_ chain of distinct types in
      the subtype relation&mdash;-that is, an infinite sequence of types
      <span class="inlinecode"><span class="id" type="var">S<sub>0</sub></span></span>, <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>, etc., such that all the <span class="inlinecode"><span class="id" type="var">Si</span></span>'s are different and
      each <span class="inlinecode"><span class="id" type="var">S</span>(<span class="id" type="var">i</span>+1)</span> is a supertype of <span class="inlinecode"><span class="id" type="var">Si</span></span>.

</li>
</ul>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_subtype_concepts_tf</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab300"></a><h4 class="section">练习：2 星, standard (proper_subtypes)</h4>
 Is the following statement true or false?  Briefly explain your
    answer.  (Here <span class="inlinecode"><span class="id" type="var">Base</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> stands for a base type, where <span class="inlinecode"><span class="id" type="var">n</span></span> is
    a string standing for the name of the base type.  See the
    Syntax section below.)

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;~(<span class="id" type="var">T</span>&nbsp;=&nbsp;<span class="id" type="var">Bool</span>&nbsp;∨&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">n</span>,&nbsp;<span class="id" type="var">T</span>&nbsp;=&nbsp;<span class="id" type="var">Base</span>&nbsp;<span class="id" type="var">n</span>)&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;&lt;:&nbsp;<span class="id" type="var">T</span>&nbsp;&nbsp;∧&nbsp;&nbsp;<span class="id" type="var">S</span>&nbsp;≠&nbsp;<span class="id" type="var">T</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_proper_subtypes</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab301"></a><h4 class="section">练习：2 星, standard (small_large_1)</h4>

<div class="paragraph"> </div>

<ul class="doclist">
<li> What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> ("smallest" in the subtype
     relation) that makes the following assertion true?  (Assume we
     have <span class="inlinecode"><span class="id" type="var">Unit</span></span> among the base types and <span class="inlinecode"><span class="id" type="var">unit</span></span> as a constant of this
     type.)

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">empty</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">p</span>:<span class="id" type="var">T</span>*<span class="id" type="var">Top</span>. <span class="id" type="var">p.fst</span>)&nbsp;((\<span class="id" type="var">z</span>:<span class="id" type="var">A.z</span>),&nbsp;<span class="id" type="var">unit</span>)&nbsp;&#x2208;&nbsp;<span class="id" type="var">A</span>→<span class="id" type="var">A</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>


</li>
<li> What is the _largest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the same assertion true?

</li>
</ul>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_small_large_1</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab302"></a><h4 class="section">练习：2 星, standard (small_large_2)</h4>

<div class="paragraph"> </div>

<ul class="doclist">
<li> What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the following
     assertion true?

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">empty</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">p</span>:(<span class="id" type="var">A</span>→<span class="id" type="var">A</span>&nbsp;*&nbsp;<span class="id" type="var">B</span>→<span class="id" type="var">B</span>). <span class="id" type="var">p</span>)&nbsp;((\<span class="id" type="var">z</span>:<span class="id" type="var">A.z</span>),&nbsp;(\<span class="id" type="var">z</span>:<span class="id" type="var">B.z</span>))&nbsp;&#x2208;&nbsp;<span class="id" type="var">T</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>


</li>
<li> What is the _largest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the same assertion true?

</li>
</ul>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_small_large_2</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab303"></a><h4 class="section">练习：2 星, standard, optional (small_large_3)</h4>

<div class="paragraph"> </div>

<ul class="doclist">
<li> What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the following
     assertion true?

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">a</span>:<span class="id" type="var">A</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">p</span>:(<span class="id" type="var">A</span>*<span class="id" type="var">T</span>). (<span class="id" type="var">p.snd</span>)&nbsp;(<span class="id" type="var">p.fst</span>))&nbsp;(<span class="id" type="var">a</span>,&nbsp;\<span class="id" type="var">z</span>:<span class="id" type="var">A.z</span>)&nbsp;&#x2208;&nbsp;<span class="id" type="var">A</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>


</li>
<li> What is the _largest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the same assertion true?

</li>
</ul>

<div class="paragraph"> </div>

 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab304"></a><h4 class="section">练习：2 星, standard (small_large_4)</h4>

<div class="paragraph"> </div>

<ul class="doclist">
<li> What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the following
     assertion true?

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">p</span>:(<span class="id" type="var">A</span>*<span class="id" type="var">T</span>). (<span class="id" type="var">p.snd</span>)&nbsp;(<span class="id" type="var">p.fst</span>))&nbsp;&#x2208;&nbsp;<span class="id" type="var">S</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>


</li>
<li> What is the _largest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the same
     assertion true?

</li>
</ul>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_small_large_4</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab305"></a><h4 class="section">练习：2 星, standard (smallest_1)</h4>
 What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the following
    assertion true?

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>&nbsp;<span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">x</span>:<span class="id" type="var">T</span>. <span class="id" type="var">x</span>&nbsp;<span class="id" type="var">x</span>)&nbsp;<span class="id" type="var">t</span>&nbsp;&#x2208;&nbsp;<span class="id" type="var">S</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_smallest_1</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab306"></a><h4 class="section">练习：2 星, standard (smallest_2)</h4>
 What is the _smallest_ type <span class="inlinecode"><span class="id" type="var">T</span></span> that makes the following
    assertion true?

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span>&nbsp;&#x22A2;&nbsp;(\<span class="id" type="var">x</span>:<span class="id" type="var">Top</span>. <span class="id" type="var">x</span>)&nbsp;((\<span class="id" type="var">z</span>:<span class="id" type="var">A.z</span>)&nbsp;,&nbsp;(\<span class="id" type="var">z</span>:<span class="id" type="var">B.z</span>))&nbsp;&#x2208;&nbsp;<span class="id" type="var">T</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_smallest_2</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab307"></a><h4 class="section">练习：3 星, standard, optional (count_supertypes)</h4>
 How many supertypes does the record type <span class="inlinecode">{<span class="id" type="var">x</span>:<span class="id" type="var">A</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">C</span>→<span class="id" type="var">C</span>}</span> have?  That is,
    how many different types <span class="inlinecode"><span class="id" type="var">T</span></span> are there such that <span class="inlinecode">{<span class="id" type="var">x</span>:<span class="id" type="var">A</span>,</span> <span class="inlinecode"><span class="id" type="var">y</span>:<span class="id" type="var">C</span>→<span class="id" type="var">C</span>}</span> <span class="inlinecode">&lt;:</span>
    <span class="inlinecode"><span class="id" type="var">T</span></span>?  (We consider two types to be different if they are written
    differently, even if each is a subtype of the other.  For example,
    <span class="inlinecode">{<span class="id" type="var">x</span>:<span class="id" type="var">A</span>,<span class="id" type="var">y</span>:<span class="id" type="var">B</span>}</span> and <span class="inlinecode">{<span class="id" type="var">y</span>:<span class="id" type="var">B</span>,<span class="id" type="var">x</span>:<span class="id" type="var">A</span>}</span> are different.)

<div class="paragraph"> </div>

 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab308"></a><h4 class="section">练习：2 星, standard (pair_permutation)</h4>
 The subtyping rule for product types
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Prod) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>*S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>*T<sub>2</sub></td>
  <td></td>
</td>
</table></center>    intuitively corresponds to the "depth" subtyping rule for records.
    Extending the analogy, we might consider adding a "permutation" rule
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">T<sub>1</sub>*T<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub>*T<sub>1</sub></td>
  <td></td>
</td>
</table></center>    for products.  Is this a good idea? Briefly explain why or why not.

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_pair_permutation</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab309"></a><h1 class="section">Formal Definitions</h1>

<div class="paragraph"> </div>

 Most of the definitions needed to formalize what we've discussed
    above &mdash; in particular, the syntax and operational semantics of
    the language &mdash; are identical to what we saw in the last chapter.
    We just need to extend the typing relation with the subsumption
    rule and add a new <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> definition for the subtyping
    relation.  Let's first do the identical bits. 
</div>

<div class="doc">
<a name="lab310"></a><h2 class="section">Core Definitions</h2>

</div>
<div class="code code-space">

<br/>
</div>

<div class="doc">
<a name="lab311"></a><h3 class="section">Syntax</h3>

<div class="paragraph"> </div>

 In the rest of the chapter, we formalize just base types,
    booleans, arrow types, <span class="inlinecode"><span class="id" type="var">Unit</span></span>, and <span class="inlinecode"><span class="id" type="var">Top</span></span>, omitting record types
    and leaving product types as an exercise.  For the sake of more
    interesting examples, we'll add an arbitrary set of base types
    like <span class="inlinecode"><span class="id" type="var">String</span></span>, <span class="inlinecode"><span class="id" type="var">Float</span></span>, etc.  (Since they are just for examples,
    we won't bother adding any operations over these base types, but
    we could easily do so.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ty</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">Top</span>   : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Bool</span>  : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Base</span>  : <span class="id" type="var">string</span> → <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Arrow</span> : <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Unit</span>  : <span class="id" type="var">ty</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tm</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">var</span> : <span class="id" type="var">string</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">app</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">abs</span> : <span class="id" type="var">string</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">tru</span> : <span class="id" type="var">tm</span> <br/>
&nbsp;&nbsp;| <span class="id" type="var">fls</span> : <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">test</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">unit</span> : <span class="id" type="var">tm</span> <br/>
.<br/>
</div>

<div class="doc">
<a name="lab312"></a><h3 class="section">Substitution</h3>

<div class="paragraph"> </div>

 The definition of substitution remains exactly the same as for the
    pure STLC. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">subst</span> (<span class="id" type="var">x</span>:<span class="id" type="var">string</span>) (<span class="id" type="var">s</span>:<span class="id" type="var">tm</span>)  (<span class="id" type="var">t</span>:<span class="id" type="var">tm</span>) : <span class="id" type="var">tm</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">var</span> <span class="id" type="var">y</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">s</span> <span class="id" type="keyword">else</span> <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>1</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T</span> (<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="keyword">else</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>))<br/>
&nbsp;&nbsp;| <span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">app</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">tru</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">tru</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">fls</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fls</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">test</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>2</sub></span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">unit</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">unit</span> <br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "'[' x ':=' s ']' t" := (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 20).<br/>
</div>

<div class="doc">
<a name="lab313"></a><h3 class="section">Reduction</h3>

<div class="paragraph"> </div>

 Likewise the definitions of the <span class="inlinecode"><span class="id" type="var">value</span></span> property and the <span class="inlinecode"><span class="id" type="var">step</span></span>
    relation. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">value</span> : <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">v_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">v_true</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">tru</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">v_false</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">fls</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">v_unit</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">unit</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">value</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Reserved Notation</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">step</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_AppAbs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>12</sub></span> <span class="id" type="var">v<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>12</sub></span>) <span class="id" type="var">v<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [<span class="id" type="var">x</span>:=<span class="id" type="var">v<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_App1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_App2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>2</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">app</span> <span class="id" type="var">v<sub>1</sub></span>  <span class="id" type="var">t<sub>2</sub>'</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_TestTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">tru</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_TestFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">fls</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Test</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
<span class="id" type="keyword">where</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" := (<span class="id" type="var">step</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">step</span>.<br/>
</div>

<div class="doc">
<a name="lab314"></a><h2 class="section">Subtyping</h2>

<div class="paragraph"> </div>

 Now we come to the interesting part.  We begin by defining
    the subtyping relation and developing some of its important
    technical properties. 
<div class="paragraph"> </div>

 The definition of subtyping is just what we sketched in the
    motivating discussion. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "T '&lt;:' U" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">subtype</span> : <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Refl</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T</span> &lt;: <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">U</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">U</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> &lt;: <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Top</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">Top</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T<sub>1</sub></span> &lt;: <span class="id" type="var">S<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S<sub>2</sub></span> &lt;: <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span>) &lt;: (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)<br/>
<span class="id" type="keyword">where</span> "T '&lt;:' U" := (<span class="id" type="var">subtype</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>).<br/>
</div>

<div class="doc">
Note that we don't need any special rules for base types (<span class="inlinecode"><span class="id" type="var">Bool</span></span>
    and <span class="inlinecode"><span class="id" type="var">Base</span></span>): they are automatically subtypes of themselves (by
    <span class="inlinecode"><span class="id" type="var">S_Refl</span></span>) and <span class="inlinecode"><span class="id" type="var">Top</span></span> (by <span class="inlinecode"><span class="id" type="var">S_Top</span></span>), and that's all we want. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">subtype</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Examples</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">string_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">x</span> := "x".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">y</span> := "y".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">z</span> := "z".<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">A</span> := (<span class="id" type="var">Base</span> "A").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">B</span> := (<span class="id" type="var">Base</span> "B").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">C</span> := (<span class="id" type="var">Base</span> "C").<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">String</span> := (<span class="id" type="var">Base</span> "String").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">Float</span> := (<span class="id" type="var">Base</span> "Float").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">Integer</span> := (<span class="id" type="var">Base</span> "Integer").<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_0</span> :<br/>
&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">Bool</span>) &lt;: (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">Top</span>).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Bool&nbsp;&lt;:&nbsp;C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Top&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab315"></a><h4 class="section">练习：2 星, standard, optional (subtyping_judgements)</h4>
 (Leave this exercise <span class="inlinecode"><span class="id" type="var">Admitted</span></span> until after you have finished adding product
    types to the language &mdash; see exercise <span class="inlinecode"><span class="id" type="var">products</span></span> &mdash; at least up to 
    this point in the file).

<div class="paragraph"> </div>

    Recall that, in chapter <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a>, the optional section
    "Encoding Records" describes how records can be encoded as pairs.
    Using this encoding, define pair types representing the following
    record types:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Person</span>&nbsp;:=&nbsp;{&nbsp;<span class="id" type="var">name</span>&nbsp;:&nbsp;<span class="id" type="var">String</span>&nbsp;}&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Student</span>&nbsp;:=&nbsp;{&nbsp;<span class="id" type="var">name</span>&nbsp;:&nbsp;<span class="id" type="var">String</span>&nbsp;;&nbsp;<span class="id" type="var">gpa</span>&nbsp;:&nbsp;<span class="id" type="var">Float</span>&nbsp;}&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Employee</span>&nbsp;:=&nbsp;{&nbsp;<span class="id" type="var">name</span>&nbsp;:&nbsp;<span class="id" type="var">String</span>&nbsp;;&nbsp;<span class="id" type="var">ssn</span>&nbsp;:&nbsp;<span class="id" type="var">Integer</span>&nbsp;}
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Person</span> : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Student</span> : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Employee</span> : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Now use the definition of the subtype relation to prove the following: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">sub_student_person</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">Student</span> &lt;: <span class="id" type="var">Person</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">sub_employee_person</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">Employee</span> &lt;: <span class="id" type="var">Person</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The following facts are mostly easy to prove in Coq.  To get
    full benefit from the exercises, make sure you also
    understand how to prove them on paper! 
<div class="paragraph"> </div>

<a name="lab316"></a><h4 class="section">练习：1 星, standard, optional (subtyping_example_1)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_1</span> :<br/>
&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">Top</span> <span class="id" type="var">Student</span>) &lt;: (<span class="id" type="var">Arrow</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">C</span>) <span class="id" type="var">Person</span>).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Student&nbsp;&lt;:&nbsp;(C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C)<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Person&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab317"></a><h4 class="section">练习：1 星, standard, optional (subtyping_example_2)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_2</span> :<br/>
&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">Top</span> <span class="id" type="var">Person</span>) &lt;: (<span class="id" type="var">Arrow</span> <span class="id" type="var">Person</span> <span class="id" type="var">Top</span>).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Person&nbsp;&lt;:&nbsp;Person<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Top&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Examples</span>.<br/>
</div>

<div class="doc">
<a name="lab318"></a><h2 class="section">Typing</h2>

<div class="paragraph"> </div>

 The only change to the typing relation is the addition of the rule
    of subsumption, <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">context</span> := <span class="id" type="var">partial_map</span> <span class="id" type="var">ty</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Reserved Notation</span> "Gamma '&#x22A2;' t '&#x2208;' T" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">has_type</span> : <span class="id" type="var">context</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Same&nbsp;as&nbsp;before&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">var</span> <span class="id" type="var">x</span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">T<sub>12</sub></span> <span class="id" type="var">t<sub>12</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">T<sub>11</sub></span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t<sub>12</sub></span> &#x2208; <span class="id" type="var">T<sub>12</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span> &#x2208; <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">T<sub>12</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_App</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_True</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">tru</span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_False</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">fls</span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Test</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> <span class="id" type="var">T</span> <span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Bool</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Unit</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">unit</span> &#x2208; <span class="id" type="var">Unit</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;New&nbsp;rule&nbsp;of&nbsp;subsumption&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Sub</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span><br/>
<br/>
<span class="id" type="keyword">where</span> "Gamma '&#x22A2;' t '&#x2208;' T" := (<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">has_type</span>.<br/>
</div>

<div class="doc">
The following hints help <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> construct typing
    derivations.  They are only used in a few places, but they give
    a nice illustration of what <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can do with a bit more 
    programming.  See chapter <a href="UseAuto.html"><span class="inlineref">UseAuto</span></a> for more on hints. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Extern</span> 2 (<span class="id" type="var">has_type</span> <span class="id" type="var">_</span> (<span class="id" type="var">app</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">_</span>) ⇒<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">T_App</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Extern</span> 2 (<span class="id" type="var">_</span> = <span class="id" type="var">_</span>) ⇒ <span class="id" type="tactic">compute</span>; <span class="id" type="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Examples2</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">Examples</span>.<br/>
</div>

<div class="doc">
Do the following exercises after you have added product types to
    the language.  For each informal typing judgement, write it as a
    formal statement in Coq and prove it. 
<div class="paragraph"> </div>

<a name="lab319"></a><h4 class="section">练习：1 星, standard, optional (typing_example_0)</h4>

</div>
<div class="code code-space">
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;((\z:A.z),&nbsp;(\z:B.z))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x2208;&nbsp;(A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A&nbsp;*&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B)&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab320"></a><h4 class="section">练习：2 星, standard, optional (typing_example_1)</h4>

</div>
<div class="code code-space">
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;(\x:(Top&nbsp;*&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B).&nbsp;x.snd)&nbsp;((\z:A.z),&nbsp;(\z:B.z))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x2208;&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab321"></a><h4 class="section">练习：2 星, standard, optional (typing_example_2)</h4>

</div>
<div class="code code-space">
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;(\z:(C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C)<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>(Top&nbsp;*&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B).&nbsp;(z&nbsp;(\x:C.x)).snd)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\z:C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C.&nbsp;((\z:A.z),&nbsp;(\z:B.z)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x2208;&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Examples2</span>.<br/>
</div>

<div class="doc">
<a name="lab322"></a><h1 class="section">Properties</h1>

<div class="paragraph"> </div>

 The fundamental properties of the system that we want to
    check are the same as always: progress and preservation.  Unlike
    the extension of the STLC with references (chapter <a href="References.html"><span class="inlineref">References</span></a>),
    we don't need to change the _statements_ of these properties to
    take subtyping into account.  However, their proofs do become a
    little bit more involved. 
</div>

<div class="doc">
<a name="lab323"></a><h2 class="section">Inversion Lemmas for Subtyping</h2>

<div class="paragraph"> </div>

 Before we look at the properties of the typing relation, we need
    to establish a couple of critical structural properties of the
    subtype relation:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">Bool</span></span> is the only subtype of <span class="inlinecode"><span class="id" type="var">Bool</span></span>, and

</li>
<li> every subtype of an arrow type is itself an arrow type. 
</li>
</ul>

<div class="paragraph"> </div>

 These are called _inversion lemmas_ because they play a
    similar role in proofs as the built-in <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic: given a
    hypothesis that there exists a derivation of some subtyping
    statement <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and some constraints on the shape of <span class="inlinecode"><span class="id" type="var">S</span></span> and/or
    <span class="inlinecode"><span class="id" type="var">T</span></span>, each inversion lemma reasons about what this derivation must
    look like to tell us something further about the shapes of <span class="inlinecode"><span class="id" type="var">S</span></span> and
    <span class="inlinecode"><span class="id" type="var">T</span></span> and the existence of subtype relations between their parts. 
<div class="paragraph"> </div>

<a name="lab324"></a><h4 class="section">练习：2 星, standard, optional (sub_inversion_Bool)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sub_inversion_Bool</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">U</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> &lt;: <span class="id" type="var">Bool</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> = <span class="id" type="var">Bool</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">U</span> <span class="id" type="var">Hs</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">Bool</span> <span class="id" type="keyword">as</span> <span class="id" type="var">V</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab325"></a><h4 class="section">练习：3 星, standard (sub_inversion_arrow)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sub_inversion_arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">U</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> &lt;: <span class="id" type="var">Arrow</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">U<sub>1</sub></span> <span class="id" type="var">U<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> = <span class="id" type="var">Arrow</span> <span class="id" type="var">U<sub>1</sub></span> <span class="id" type="var">U<sub>2</sub></span> ∧ <span class="id" type="var">V<sub>1</sub></span> &lt;: <span class="id" type="var">U<sub>1</sub></span> ∧ <span class="id" type="var">U<sub>2</sub></span> &lt;: <span class="id" type="var">V<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">U</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span> <span class="id" type="var">Hs</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">V</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">V<sub>2</sub></span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">V<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab326"></a><h2 class="section">Canonical Forms</h2>

<div class="paragraph"> </div>

 The proof of the progress theorem &mdash; that a well-typed
    non-value can always take a step &mdash; doesn't need to change too
    much: we just need one small refinement.  When we're considering
    the case where the term in question is an application <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
    where both <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> are values, we need to know that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> has
    the _form_ of a lambda-abstraction, so that we can apply the
    <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span> reduction rule.  In the ordinary STLC, this is
    obvious: we know that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> has a function type <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span>→<span class="id" type="var">T<sub>12</sub></span></span>, and
    there is only one rule that can be used to give a function type to
    a value &mdash; rule <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> &mdash; and the form of the conclusion of this
    rule forces <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> to be an abstraction.

<div class="paragraph"> </div>

    In the STLC with subtyping, this reasoning doesn't quite work
    because there's another rule that can be used to show that a value
    has a function type: subsumption.  Fortunately, this possibility
    doesn't change things much: if the last rule used to show <span class="inlinecode"><span class="id" type="var">Gamma</span></span>
    <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>11</sub></span>→<span class="id" type="var">T<sub>12</sub></span></span> is subsumption, then there is some
    _sub_-derivation whose subject is also <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>, and we can reason by
    induction until we finally bottom out at a use of <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>.

<div class="paragraph"> </div>

    This bit of reasoning is packaged up in the following lemma, which
    tells us the possible "canonical forms" (i.e., values) of function
    type. 
<div class="paragraph"> </div>

<a name="lab327"></a><h4 class="section">练习：3 星, standard, optional (canonical_forms_of_arrow_types)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">canonical_forms_of_arrow_types</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">s</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">s</span> &#x2208; <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Similarly, the canonical forms of type <span class="inlinecode"><span class="id" type="var">Bool</span></span> are the constants
    <span class="inlinecode"><span class="id" type="var">tru</span></span> and <span class="inlinecode"><span class="id" type="var">fls</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">canonical_forms_of_Bool</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">s</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">s</span> &#x2208; <span class="id" type="var">Bool</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">tru</span> ∨ <span class="id" type="var">s</span> = <span class="id" type="var">fls</span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">s</span> <span class="id" type="var">Hty</span> <span class="id" type="var">Hv</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">Bool</span> <span class="id" type="keyword">as</span> <span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">sub_inversion_Bool</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">subst</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab328"></a><h2 class="section">Progress</h2>

<div class="paragraph"> </div>

 The proof of progress now proceeds just like the one for the
    pure STLC, except that in several places we invoke canonical forms
    lemmas... 
<div class="paragraph"> </div>

 _Theorem_ (Progress): For any term <span class="inlinecode"><span class="id" type="var">t</span></span> and type <span class="inlinecode"><span class="id" type="var">T</span></span>, if <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span>
    <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> then <span class="inlinecode"><span class="id" type="var">t</span></span> is a value or <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t'</span></span>.

<div class="paragraph"> </div>

    _Proof_: Let <span class="inlinecode"><span class="id" type="var">t</span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> be given, with <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  Proceed
    by induction on the typing derivation.

<div class="paragraph"> </div>

    The cases for <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, <span class="inlinecode"><span class="id" type="var">T_Unit</span></span>, <span class="inlinecode"><span class="id" type="var">T_True</span></span> and <span class="inlinecode"><span class="id" type="var">T_False</span></span> are
    immediate because abstractions, <span class="inlinecode"><span class="id" type="var">unit</span></span>, <span class="inlinecode"><span class="id" type="var">tru</span></span>, and <span class="inlinecode"><span class="id" type="var">fls</span></span> are
    already values.  The <span class="inlinecode"><span class="id" type="var">T_Var</span></span> case is vacuous because variables
    cannot be typed in the empty context.  The remaining cases are
    more interesting:

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last step in the typing derivation uses rule <span class="inlinecode"><span class="id" type="var">T_App</span></span>,
      then there are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> such that
      <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span>
      <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>.  Moreover, by the induction hypothesis, either <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is
      a value or it steps, and either <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a value or it steps.
      There are three possibilities to consider:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>.  Then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
        by <span class="inlinecode"><span class="id" type="var">ST_App1</span></span>.

<div class="paragraph"> </div>


</li>
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span>.
        Then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span> by rule <span class="inlinecode"><span class="id" type="var">ST_App2</span></span> because <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a
        value.

<div class="paragraph"> </div>


</li>
<li> Finally, suppose <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> are both values.  By the
        canonical forms lemma for arrow types, we know that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> has the
        form <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.s2</span></span> for some <span class="inlinecode"><span class="id" type="var">x</span></span>, <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>.  But then
        <span class="inlinecode">(\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.s2</span>)</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">s<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>, since <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a
        value.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the final step of the derivation uses rule <span class="inlinecode"><span class="id" type="var">T_Test</span></span>, then there
      are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span>
      <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, with <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span> and with <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and
      <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  Moreover, by the induction hypothesis,
      either <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value or it steps.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value, then by the canonical forms lemma for
         booleans, either <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">tru</span></span> or <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">fls</span></span>.  In either
         case, <span class="inlinecode"><span class="id" type="var">t</span></span> can step, using rule <span class="inlinecode"><span class="id" type="var">ST_TestTrue</span></span> or <span class="inlinecode"><span class="id" type="var">ST_TestFalse</span></span>.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> can step, then so can <span class="inlinecode"><span class="id" type="var">t</span></span>, by rule <span class="inlinecode"><span class="id" type="var">ST_Test</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>, then there is
      a type <span class="inlinecode"><span class="id" type="var">S</span></span> such that <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">S</span></span>.  The desired
      result is exactly the induction hypothesis for the typing
      subderivation.

</li>
</ul>
    Formally: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">empty</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">revert</span> <span class="id" type="var">HeqGamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">HeqGamma</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt2</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">canonical_forms_of_arrow_types</span> <span class="id" type="var">empty</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">x</span> [<span class="id" type="var">S<sub>1</sub></span> [<span class="id" type="var">t<sub>12</sub></span> <span class="id" type="var">Heqt1</span>]]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span style='font-size:120%;'>&exist;</span>([<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>2</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">assert</span> (<span class="id" type="var">t<sub>1</sub></span> = <span class="id" type="var">tru</span> ∨ <span class="id" type="var">t<sub>1</sub></span> = <span class="id" type="var">fls</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> (<span class="id" type="tactic">eapply</span> <span class="id" type="var">canonical_forms_of_Bool</span>; <span class="id" type="tactic">eauto</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rename</span> <span class="id" type="var">x</span> <span class="id" type="var">into</span> <span class="id" type="var">t<sub>1</sub>'</span>. <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab329"></a><h2 class="section">Inversion Lemmas for Typing</h2>

<div class="paragraph"> </div>

 The proof of the preservation theorem also becomes a little more
    complex with the addition of subtyping.  The reason is that, as
    with the "inversion lemmas for subtyping" above, there are a
    number of facts about the typing relation that are immediate from
    the definition in the pure STLC (formally: that can be obtained
    directly from the <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic) but that require real proofs
    in the presence of subtyping because there are multiple ways to
    derive the same <span class="inlinecode"><span class="id" type="var">has_type</span></span> statement.

<div class="paragraph"> </div>

    The following inversion lemma tells us that, if we have a
    derivation of some typing statement <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.t2</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> whose
    subject is an abstraction, then there must be some subderivation
    giving a type to the body <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>. 
<div class="paragraph"> </div>

 _Lemma_: If <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.t2</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>, then there is a type <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span>
    such that <span class="inlinecode"><span class="id" type="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" type="var">S<sub>1</sub></span>;</span> <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

    (Notice that the lemma does _not_ say, "then <span class="inlinecode"><span class="id" type="var">T</span></span> itself is an arrow
    type" &mdash; this is tempting, but false!)

<div class="paragraph"> </div>

    _Proof_: Let <span class="inlinecode"><span class="id" type="var">Gamma</span></span>, <span class="inlinecode"><span class="id" type="var">x</span></span>, <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> be given as
     described.  Proceed by induction on the derivation of <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span>
     <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.t2</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  Cases <span class="inlinecode"><span class="id" type="var">T_Var</span></span>, <span class="inlinecode"><span class="id" type="var">T_App</span></span>, are vacuous as those
     rules cannot be used to give a type to a syntactic abstraction.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last step of the derivation is a use of <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> then
       there is a type <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> and <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub></span>;</span>
       <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span>.  Picking <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> for <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> gives us what we
       need: <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>12</sub></span></span> follows from <span class="inlinecode"><span class="id" type="var">S_Refl</span></span>.

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last step of the derivation is a use of <span class="inlinecode"><span class="id" type="var">T_Sub</span></span> then
       there is a type <span class="inlinecode"><span class="id" type="var">S</span></span> such that <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.t2</span></span>
       <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">S</span></span>.  The IH for the typing subderivation tells us that there
       is some type <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> with <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S</span></span> and <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub></span>;</span> <span class="inlinecode"><span class="id" type="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
       <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span>.  Picking type <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> gives us what we need, since <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">→</span>
       <span class="inlinecode"><span class="id" type="var">S<sub>2</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> then follows by <span class="inlinecode"><span class="id" type="var">S_Trans</span></span>.

</li>
</ul>

<div class="paragraph"> </div>

    Formally: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Arrow</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span> &lt;: <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;∧ (<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">S<sub>1</sub></span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">S<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>12</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHhas_type</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">S<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty</span>]]...<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Similarly... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; (<span class="id" type="var">var</span> <span class="id" type="var">x</span>) &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">S</span> ∧ <span class="id" type="var">S</span> &lt;: <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U</span> [<span class="id" type="var">Hctx</span> <span class="id" type="var">HsubU</span>]]... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_app</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) &#x2208; <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U<sub>1</sub></span> [<span class="id" type="var">Hty1</span> <span class="id" type="var">Hty2</span>]]...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">tru</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Bool</span> &lt;: <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">T</span> <span class="id" type="var">Htyp</span>. <span class="id" type="var">remember</span> <span class="id" type="var">tru</span> <span class="id" type="keyword">as</span> <span class="id" type="var">tu</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqtu</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">fls</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Bool</span> &lt;: <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">T</span> <span class="id" type="var">Htyp</span>. <span class="id" type="var">remember</span> <span class="id" type="var">fls</span> <span class="id" type="keyword">as</span> <span class="id" type="var">tu</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqtu</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_if</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>) &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;∧ <span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;∧ <span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> <span class="id" type="var">T</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHty</span> <span class="id" type="var">H<sub>0</sub></span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">H<sub>1</sub></span> [<span class="id" type="var">H<sub>2</sub></span> <span class="id" type="var">H<sub>3</sub></span>]]...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_unit</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">unit</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Unit</span> &lt;: <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">T</span> <span class="id" type="var">Htyp</span>. <span class="id" type="var">remember</span> <span class="id" type="var">unit</span> <span class="id" type="keyword">as</span> <span class="id" type="var">tu</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqtu</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
The inversion lemmas for typing and for subtyping between arrow
    types can be packaged up as a useful "combination lemma" telling
    us exactly what we'll actually require below. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">abs_arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">empty</span> &#x22A2; (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>) &#x2208; (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T<sub>1</sub></span> &lt;: <span class="id" type="var">S<sub>1</sub></span><br/>
&nbsp;&nbsp;∧ (<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">S<sub>1</sub></span> ; <span class="id" type="var">empty</span>) &#x22A2; <span class="id" type="var">s<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">typing_inversion_abs</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">S<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty1</span>]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">sub_inversion_arrow</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hsub</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hsub</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U<sub>1</sub></span> [<span class="id" type="var">U<sub>2</sub></span> [<span class="id" type="var">Heq</span> [<span class="id" type="var">Hsub1</span> <span class="id" type="var">Hsub2</span>]]]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heq</span>; <span class="id" type="tactic">subst</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab330"></a><h2 class="section">Context Invariance</h2>

<div class="paragraph"> </div>

 The context invariance lemma follows the same pattern as in the
    pure STLC. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">appears_free_in</span> : <span class="id" type="var">string</span> → <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> → <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>2</sub></span> → <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">y</span> ≠ <span class="id" type="var">x</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>12</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_test1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_test2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_test3</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>3</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">appears_free_in</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">context_invariance</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">Gamma'</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> → <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Gamma'</span> <span class="id" type="var">x</span>)  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma'</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span>.<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma'</span> <span class="id" type="var">Heqv</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Var</span>... <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Heqv</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>... <span class="id" type="tactic">apply</span> <span class="id" type="var">IHhas_type</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">x<sub>0</sub></span> <span class="id" type="var">Hafi</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">x<sub>0</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Test</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">free_in_context</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T'</span>, <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">T'</span>.<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">Hafi</span> <span class="id" type="var">Htyp</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hafi</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHtyp</span> <span class="id" type="var">H<sub>4</sub></span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">T</span> <span class="id" type="var">Hctx</span>]. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">eqb_string_false_iff</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>2</sub></span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab331"></a><h2 class="section">Substitution</h2>

<div class="paragraph"> </div>

 The _substitution lemma_ is proved along the same lines as
    for the pure STLC.  The only significant change is that there are
    several places where, instead of the built-in <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic,
    we need to use the inversion lemmas that we proved above to
    extract structural information from assumptions about the
    well-typedness of subterms. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">substitution_preserves_typing</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">U</span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> &#x22A2; <span class="id" type="var">v</span> &#x2208; <span class="id" type="var">U</span>   →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; [<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span>.<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span> <span class="id" type="var">Htypt</span> <span class="id" type="var">Htypv</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">S</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">t</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">s</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_var</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T</span> [<span class="id" type="var">Hctx</span> <span class="id" type="var">Hsub</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">Hxy</span>|<span class="id" type="var">Hxy</span>]; <span class="id" type="tactic">eauto</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hctx</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">clear</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">context_invariance</span> <span class="id" type="keyword">with</span> <span class="id" type="var">empty</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hcontra</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">free_in_context</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">S</span> <span class="id" type="var">empty</span> <span class="id" type="var">Hcontra</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T'</span> <span class="id" type="var">HT'</span>]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HT'</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;app&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_app</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T<sub>1</sub></span> [<span class="id" type="var">Htypt1</span> <span class="id" type="var">Htypt2</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">T_App</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">s</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>. <span class="id" type="tactic">rename</span> <span class="id" type="var">t</span> <span class="id" type="var">into</span> <span class="id" type="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_abs</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Htypt2</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Sub</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)... <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">Hxy</span>|<span class="id" type="var">Hxy</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_string</span> <span class="id" type="var">y</span> <span class="id" type="var">x</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHt</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">z</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">eqb_string_false_iff</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hxy</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hxy</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;tru&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Bool</span> &lt;: <span class="id" type="var">S</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> (<span class="id" type="var">typing_inversion_true</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>  <span class="id" type="var">Htypt</span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;fls&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Bool</span> &lt;: <span class="id" type="var">S</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> (<span class="id" type="var">typing_inversion_false</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>  <span class="id" type="var">Htypt</span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span>  ((<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">U</span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;∧  (<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">U</span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">S</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;∧  (<span class="id" type="var">x</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">U</span> ; <span class="id" type="var">Gamma</span>) &#x22A2; <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">S</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> (<span class="id" type="var">typing_inversion_if</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">H<sub>1</sub></span> [<span class="id" type="var">H<sub>2</sub></span> <span class="id" type="var">H<sub>3</sub></span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHt1</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHt2</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHt3</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>3</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;unit&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Unit</span> &lt;: <span class="id" type="var">S</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> (<span class="id" type="var">typing_inversion_unit</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>  <span class="id" type="var">Htypt</span>)...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab332"></a><h2 class="section">Preservation</h2>

<div class="paragraph"> </div>

 The proof of preservation now proceeds pretty much as in earlier
    chapters, using the substitution lemma at the appropriate point
    and again using inversion lemmas from above to extract structural
    information from typing assumptions. 
<div class="paragraph"> </div>

 _Theorem_ (Preservation): If <span class="inlinecode"><span class="id" type="var">t</span></span>, <span class="inlinecode"><span class="id" type="var">t'</span></span> are terms and <span class="inlinecode"><span class="id" type="var">T</span></span> is a type
    such that <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span>, then <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">&#x2208;</span>
    <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

    _Proof_: Let <span class="inlinecode"><span class="id" type="var">t</span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> be given such that <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  We
    proceed by induction on the structure of this typing derivation,
    leaving <span class="inlinecode"><span class="id" type="var">t'</span></span> general.  The cases <span class="inlinecode"><span class="id" type="var">T_Abs</span></span>, <span class="inlinecode"><span class="id" type="var">T_Unit</span></span>, <span class="inlinecode"><span class="id" type="var">T_True</span></span>, and
    <span class="inlinecode"><span class="id" type="var">T_False</span></span> cases are vacuous because abstractions and constants
    don't step.  Case <span class="inlinecode"><span class="id" type="var">T_Var</span></span> is vacuous as well, since the context is
    empty.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then there
       are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> such that
       <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, and
       <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

       By the definition of the step relation, there are three ways
       <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> can step.  Cases <span class="inlinecode"><span class="id" type="var">ST_App1</span></span> and <span class="inlinecode"><span class="id" type="var">ST_App2</span></span> follow
       immediately by the induction hypotheses for the typing
       subderivations and a use of <span class="inlinecode"><span class="id" type="var">T_App</span></span>.

<div class="paragraph"> </div>

       Suppose instead <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> steps by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>.  Then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span>
       <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S.t12</span></span> for some type <span class="inlinecode"><span class="id" type="var">S</span></span> and term <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span>
       <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span></span>.

<div class="paragraph"> </div>

       By lemma <span class="inlinecode"><span class="id" type="var">abs_arrow</span></span>, we have <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S</span></span> and <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>.
       It then follows by the substitution lemma
       (<span class="inlinecode"><span class="id" type="var">substitution_preserves_typing</span></span>) that <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]</span>
       <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> as desired.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the final step of the derivation uses rule <span class="inlinecode"><span class="id" type="var">T_Test</span></span>, then
        there are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span>
        <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, with <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span> and with <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
        <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  Moreover, by the induction
        hypothesis, if <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> steps to <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> then <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>.
        There are three cases to consider, depending on which rule was
        used to show <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> by rule <span class="inlinecode"><span class="id" type="var">ST_Test</span></span>, then <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
             <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> with <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>.  By the induction hypothesis,
             <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>, and so <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> by
             <span class="inlinecode"><span class="id" type="var">T_Test</span></span>.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> by rule <span class="inlinecode"><span class="id" type="var">ST_TestTrue</span></span> or <span class="inlinecode"><span class="id" type="var">ST_TestFalse</span></span>, then
             either <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> or <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>
             follows by assumption.

<div class="paragraph"> </div>


</li>
</ul>

</li>
</ul>

</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>, then there
       is a type <span class="inlinecode"><span class="id" type="var">S</span></span> such that <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">S</span></span>.  The
       result is immediate by the induction hypothesis for the typing
       subderivation and an application of <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>.  <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty</span> &#x22A2; <span class="id" type="var">t'</span> &#x2208; <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')"><span class="show"></span></div>
<div class="proofscript" id="proof17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">empty</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">HeqGamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t'</span> <span class="id" type="var">HeqGamma</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">abs_arrow</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">HT<sub>1</sub></span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">HA<sub>1</sub></span> <span class="id" type="var">HA<sub>2</sub></span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">substitution_preserves_typing</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab333"></a><h2 class="section">Records, via Products and Top</h2>

<div class="paragraph"> </div>

 This formalization of the STLC with subtyping omits record
    types for brevity.  If we want to deal with them more seriously,
    we have two choices.

<div class="paragraph"> </div>

    First, we can treat them as part of the core language, writing
    down proper syntax, typing, and subtyping rules for them.  Chapter
    <span class="inlinecode"><span class="id" type="var">RecordSub</span></span> shows how this extension works.

<div class="paragraph"> </div>

    On the other hand, if we are treating them as a derived form that
    is desugared in the parser, then we shouldn't need any new rules:
    we should just check that the existing rules for subtyping product
    and <span class="inlinecode"><span class="id" type="var">Unit</span></span> types give rise to reasonable rules for record
    subtyping via this encoding. To do this, we just need to make one
    small change to the encoding described earlier: instead of using
    <span class="inlinecode"><span class="id" type="var">Unit</span></span> as the base case in the encoding of tuples and the "don't
    care" placeholder in the encoding of records, we use <span class="inlinecode"><span class="id" type="var">Top</span></span>.  So:
<pre>
    {a:Nat, b:Nat} --<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> {Nat,Nat}       i.e., (Nat,(Nat,Top))
    {c:Nat, a:Nat} --<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> {Nat,Top,Nat}   i.e., (Nat,(Top,(Nat,Top)))
</pre>
    The encoding of record values doesn't change at all.  It is
    easy (and instructive) to check that the subtyping rules above are
    validated by the encoding. 
</div>

<div class="doc">
<a name="lab334"></a><h2 class="section">Exercises</h2>

<div class="paragraph"> </div>

<a name="lab335"></a><h4 class="section">练习：2 星, standard (variations)</h4>
 Each part of this problem suggests a different way of changing the
    definition of the STLC with Unit and subtyping.  (These changes
    are not cumulative: each part starts from the original language.)
    In each part, list which properties (Progress, Preservation, both,
    or neither) become false.  If a property becomes false, give a
    counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose we add the following typing rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;S<sub>1</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>S<sub>2</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;T<sub>1</sub>&nbsp;<:&nbsp;S<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (T_Funny1) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma&nbsp;&#x22A2;&nbsp;t&nbsp;&#x2208;&nbsp;T<sub>1</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>T<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we add the following reduction rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Funny21) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">unit&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(\x:Top.&nbsp;x)</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we add the following subtyping rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Funny3) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Unit&nbsp;<:&nbsp;Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Top</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we add the following subtyping rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (S_Funny4) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Top&nbsp;<:&nbsp;Unit</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we add the following reduction rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Funny5) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(unit&nbsp;t)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(t&nbsp;unit)</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we add the same reduction rule _and_ a new typing rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Funny5) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(unit&nbsp;t)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(t&nbsp;unit)</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Funny6) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">empty&nbsp;&#x22A2;&nbsp;unit&nbsp;&#x2208;&nbsp;Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Top</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Suppose we _change_ the arrow subtyping rule to:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Arrow') &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>T<sub>2</sub></td>
  <td></td>
</td>
</table></center>
</li>
</ul>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_variations</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab336"></a><h1 class="section">Exercise: Adding Products</h1>

<div class="paragraph"> </div>

<a name="lab337"></a><h4 class="section">练习：5 星, standard (products)</h4>
 Adding pairs, projections, and product types to the system we have
    defined is a relatively straightforward matter.  Carry out this
    extension by modifying the definitions and proofs above:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Add constructors for pairs, first and second projections,
      and product types to the definitions of <span class="inlinecode"><span class="id" type="var">ty</span></span> and <span class="inlinecode"><span class="id" type="var">tm</span></span>, and
      extend the surrounding definitions accordingly
      (refer to chapter <a href="MoreSTLC.html"><span class="inlineref">MoreSTLC</span></a>):

<div class="paragraph"> </div>

<ul class="doclist">
<li> value relation

</li>
<li> substitution

</li>
<li> operational semantics

</li>
<li> typing relation

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> Extend the subtyping relation with this rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (S_Prod) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">S<sub>1</sub>&nbsp;*&nbsp;S<sub>2</sub>&nbsp;<:&nbsp;T<sub>1</sub>&nbsp;*&nbsp;T<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


</li>
<li> Extend the proofs of progress, preservation, and all their
      supporting lemmas to deal with the new constructs.  (You'll also
      need to add a couple of completely new lemmas.) 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_products</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:15:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>